ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), n:. ecl-halt(ds;da;x)(n,nil)  False 

latex

Definitions	x:A. B(x), , P  Q, ecl-halt(ds;da;x), False, Prop, P  Q, t  T, x. t(x), P & Q, x:A. B(x), A, P  Q, AB, P  Q, event-info(ds;da), Valtype(da;k), let x,y,z = a in t(x;y;z), A & B, SQType(T), {T}, x(s), ||as||, Y, as @ bs, Dec(P), star-append(T;P;Q), (xL.P(x))
Lemmas	ecl-induction, nat wf, iff wf, ecl-halt wf, event-info wf, false wf, ecl wf, decl-state wf, ma-valtype wf, append wf, assert wf, l all wf, not wf, bool wf, le wf, iseg wf, star-append wf, l member wf, l exists wf, fpf wf, Knd wf, Id wf, append is nil, length wf1, Knd sq, decidable false, decidable lt, concat wf